Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add JSON support for VerificationResults #93

Open
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

TrisCC
Copy link
Collaborator

@TrisCC TrisCC commented Jun 26, 2024

Changes:

  • Add JSON support for VerificationResults: Working with csvs was fine, but to read some of the error messages from a few instances manually to inspect errors was a bit difficult. JSON is more suitable for that.
  • Fix relative import
  • Improve logger and json converter: Add a little indicator to see how far into the verification batch process the program is in.

@TrisCC TrisCC closed this Jul 3, 2024
@TrisCC TrisCC reopened this Jul 3, 2024
@TrisCC TrisCC changed the title Add JSON support and fix VeriNet installer Add JSON support Jul 16, 2024
@TrisCC TrisCC changed the title Add JSON support Add JSON support for VerificationResults Jul 26, 2024
@TrisCC TrisCC closed this Jul 29, 2024
@TrisCC TrisCC reopened this Jul 29, 2024
res_d = result.unwrap_err()
success = "ERR"

inst_d = {
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think these abbrevations like inst_d and vdr are not so readable. I would rather put the full names for readability

@@ -22,6 +23,7 @@
class VerificationDataResult:
"""_summary_."""

# TODO: Convert files to path objects
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would not put todos in the code. I would rather create an issue from this

"success": self.success,
"result": self.result,
"took": str(self.took),
# "counter_example": self.counter_example or "",
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would not publish commented code

"network": str(self.network),
"property": str(self.property),
"timeout": str(self.timeout),
"verifier": self.verifier,
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why are the verifier, success and result not wrapped into str()?

def json_write_verification_result(
verification_result: VerificationDataResult, json_path: Path
):
"""_summary_."""
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't this summary be changed to contain some information?

file_data = {"instances": []}

file_data["instances"].append(verification_result.as_json_row())
json_file.seek(0)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this necessary?

json_path: Path,
) -> list[VerificationDataResult]:
"""Reads a verification results json to a list of its dataclass."""
results = pd.read_json(json_path)["instances"].tolist()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Shouldn't we maybe use the json package for parsing the json here? Pandas can quite easily break for parsing jsons. Also were will an error occuring here be catched?

@@ -58,6 +60,25 @@ def as_csv_row(self) -> list[str]:
self.stdout or "",
]

def as_json_row(self) -> dict[str, Any]:
"""Convert data to a json item."""
if isinstance(self.counter_example, tuple):
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do we still need this, if the counter example is not returned?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants